lambda cube
單純型附きλ計算 (simply-typed lambda calculus)$ \lambda\to
項に依存した項。一階命題論理
三軸
多相型 (polymorphism)$ \lambda 2 型に依存した項。二階命題論理
parametric 多相
型演算 (type operators)$ \lambda\underline\omega 型に依存した型。弱性高階命題論理
依存型 (dependent type)$ \lambda\Pi 三軸全てを備へた calculus of constructions (CoC)$ \lambda C